A, B:Realizer. R-Feasible(A)  R-Feasible(B)  A || B  [[A]] || [[B]] 

latex

Definitions	False, A, True, T, ff, P  Q, P & Q, , P  Q, tt, if b then t else f fi , t  T, A  B, P  Q, x:A. B(x), Unit, , , A c B, , S  T
Lemmas	es realizer wf, R-Feasible wf, R-compat wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, bnot wf, lt int wf, assert of le int, eqtt to assert, le wf, assert wf, iff transitivity, bool wf, nat plus inc, nat wf, nat plus wf, R-size wf, le int wf, ifthenelse wf, R-compat-Dsys